\begin{tabbing}
conditional{-}send{-}p(${\it es}$;${\it ds}$;$k$;$B$;$l$;${\it tg}$;$T$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\forall$$x$:Id. es{-}vartype(${\it es}$; source($l$); $x$) $\subseteq$r fpf{-}cap(${\it ds}$;IdDeq;$x$;Top))\+
\\[0ex]\& (\=$\forall$$e$:es{-}E(${\it es}$).\+
\\[0ex](es{-}loc(${\it es}$; $e$) = source($l$) $\in$ Id)
\\[0ex]$\Rightarrow$ (es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd)
\\[0ex]$\Rightarrow$ (es{-}valtype(${\it es}$; $e$) $\subseteq$r $B$))
\-\\[0ex]\& ($\forall$$e$:es{-}E(${\it es}$). (es{-}kind(${\it es}$; $e$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ (es{-}valtype(${\it es}$; $e$) $\subseteq$r $T$)))
\\[0ex]c$\wedge$ \=($\forall$$e$:es{-}E(${\it es}$).\+
\\[0ex](es{-}loc(${\it es}$; $e$) = source($l$) $\in$ Id)
\\[0ex]$\Rightarrow$ (es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd)
\\[0ex]$\Rightarrow$ \=((\=($\uparrow$can{-}apply($f$;$<$es{-}state{-}when(${\it es}$;$e$), es{-}val(${\it es}$; $e$)$>$))\+\+
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex]((es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$) $\in$ Knd)
\\[0ex]c$\wedge$ \=(es{-}sender(${\it es}$; ${\it e'}$) = $e$ $\in$ es{-}E(${\it es}$)\+
\\[0ex]\& (\=$\forall$${\it e''}$:es{-}E(${\it es}$).\+
\\[0ex](es{-}kind(${\it es}$; ${\it e''}$) = rcv($l$,${\it tg}$) $\in$ Knd)
\\[0ex]$\Rightarrow$ (es{-}sender(${\it es}$; ${\it e''}$) = $e$ $\in$ es{-}E(${\it es}$))
\\[0ex]$\Rightarrow$ (${\it e''}$ = ${\it e'}$ $\in$ es{-}E(${\it es}$)))
\-\\[0ex]\& \=es{-}val(${\it es}$; ${\it e'}$)\+
\\[0ex]=
\\[0ex]do{-}apply($f$;$<$es{-}state{-}when(${\it es}$;$e$), es{-}val(${\it es}$; $e$)$>$)
\\[0ex]$\in$ $T$))))
\-\-\-\-\\[0ex]\& (\=($\neg$($\uparrow$can{-}apply($f$;$<$es{-}state{-}when(${\it es}$;$e$), es{-}val(${\it es}$; $e$)$>$)))\+
\\[0ex]$\Rightarrow$ ($\neg$($\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex]((es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$) $\in$ Knd)
\\[0ex]c$\wedge$ (es{-}sender(${\it es}$; ${\it e'}$) = $e$ $\in$ es{-}E(${\it es}$))))))))
\-\-\-\-\-
\end{tabbing}